Section: New Results

Formal study of a triangulation algorithm

Participant : Yves Bertot.

We wish to describe a triangulation algorithm in a way that respects both a high level of abstraction and a precise account of pointer manipulations. Using refinements approaches as in CoqEAL, we hope that this can lead to efficient implementation that are derived from the formal description.